In this paper we define Martin-L¨of complexes to be algebras for monads on the category of (reflexive) globular sets which freely add cells in accordance with the rules of intensional Martin-L¨of type theory. We then study the resulting categories of algebras for several theories. Our principal result is that there exists a cofibrantly generated Quillen model structure on the category of 1-truncated Martin-L¨of complexes and that this category is Quillen equivalent to the category of groupoids. In particular, 1-truncated Martin-L¨of complexes (...) are a model of homotopy 1-types. In order to establish these facts we give a proof-theoretic analysis, using a modified version of Tait’s logical predicates argument, of the propositional equality classes of terms of identity type in the 1-truncated theory. (shrink)

We present a solution to the problem of defining a counterpart in Algebraic Set Theory of the construction of internal sheaves in Topos Theory. Our approach is general in that we consider sheaves as determined by Lawvere-Tierney coverages, rather than by Grothendieck coverages, and assume only a weakening of the axioms for small maps originally introduced by Joyal and Moerdijk, thus subsuming the existing topos-theoretic results.